COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<cs258.1[w84,jmc]		CS258 handout>>
C00006 ENDMK
C⊗;
.<<cs258.1[w84,jmc]		CS258 handout>>
.require "memo.pub[let,jmc]" source;
.turn on "→"
→{date}
.cb CS258 Handout 1

Here is the problem from the CS206 take-home.

4.	%2sublis[pattern, alist]%1 is the result of making the
substitutions described in ⊗alist in ⊗pattern.  Thus

%2sublis%1[(PLUS X (TIMES X Y) A), ((X.A) (Y.(PLUS X Y)))] 
		= (PLUS A (TIMES A (PLUS X Y)) A)

%2match[pattern,expression,alist]%1 attempts to match ⊗pattern against
⊗expression to produce and extension of ⊗alist such that substituting
in the pattern according to the result will give back %2expression%1.
If the match is unsuccessful, the value is the atom NO.  It is assumed
that a predicate  ⊗isvar  applicable to atoms is available that distinguishes
variables from other atoms.  Assuming that ⊗X and ⊗Y are variables, we have

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),qnil] = ((X.A) (Y TIMES B C)),

and

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),((X.B))] = NO.

a. Write recursive programs for ⊗sublis and ⊗match. 

b. Write accurately the sentence that expresses the fact that
⊗sublis and ⊗match are partial inverses.

c. Prove the sentence of part b.

Here is what I had in mind for the solutions of parts a and b.  Part c
is accomplished by S-expression induction on the structure of  %2pat%1.
Our problem is to set this up in EKL.  It is in order for students to
work together on it.

.begin verbatim

sublis[pat,alist] ← if at pat
		    then [if isvar pat
			  then {assoc[pat,alist}[λz. if n z
							then error[]
							else d z]
			  else pat]
		    else sublis[a pat,alist].sublis[d pat,alist]

match[pat,exp,alist] ← if alist = NO
		       then NO
		       else if at pat
		       then [if isvar pat
			     then {assoc[pat,alist]}
				  [λz.if n z
				      then [pat.exp].alist
				      else [if d z = exp
					    then alist
					    else NO]]
			      else [if pat = exp then alist else NO]]
			else if at exp then NO
			else match[d pat,d exp,match[a pat,a exp,alist]]

∀pat exp alist. match[pat,exp,alist] ≠ NO
		 ⊃ sublis[pat,match[pat,exp,alist]] = exp

.end

	Attached also is Ian Mason's solution of the problem.  It seemed to
me to be the clearest of those submitted.